Nuprl Definition : dset_set
13,42
postcript
pdf
{
x
:
s
|
Q
(
x
) } == mk_dset({
x
:|
s
||
Q
(
x
)} , =
)
latex
clarification:
{
x
:
s
|
Q
(
x
) } == mk_dset({
x
:|
s
||
Q
(
x
)} , =
s
)
latex
Up
sets
1
Wellformedness Lemmas
dset
set
wf
Definitions
mk_dset(
T
,
eq
)
,
|
p
|
,
=
origin
)
s) )
s)